package tableaux.backjumping;

//import java.util.Collections;
import java.util.HashSet;
import java.util.Set;
import java.util.Stack;

import tableaux.Branching;
import tableaux.Completion;
import tableaux.Completion.InQueueOrder;
import utils.exception.BackjumpingNoDepSetException;

import entities.Individual;
import entities.concept.Concept;

/***
 * Given a node with clashes, try the next branching node if any.
 * 
 * @author j55wu
 * 
 */
public class Backjumping {
	private Completion dc;

	public Backjumping(Completion dc) {
		this.dc = dc;
	}

	/**
	 * Note that the clashes can be caused by a single concept, e.g., ~top,
	 * bottom, etc.
	 * 
	 * @param ind
	 * @param clashes
	 * @throws BackjumpingNoDepSetException
	 */
	public boolean hasNextBranching(Individual ind, Set<Concept> clashes)
			throws BackjumpingNoDepSetException {
		Set<Integer> ais = new HashSet<Integer>();
		for (Concept c : clashes) {
			if (Completion.DEP_MAX) {
				int i = DependencyImpMax.getDepOfConcept(ind, c);
				if (i > 0) {
					ais.add(i);
				}
			} else {
				ais.addAll(DependencyImp.getDepSetOfConcept(ind, c));
			}

		}
		if (ais.size() < 1) {
			return false;
		}
		// check if needs to further explore the current branch
		return hasNextBranchingOd(ind, ais);
	}

	private boolean hasNextBranchingOd(Individual ind, Set<Integer> ais)
			throws BackjumpingNoDepSetException {
		Branching cur = this.dc.getCurrentBranching();
		if (cur == null) {
			return false;
		}
		Integer ci = cur.getOrder();
		if (ais.contains(ci)) {
			// continue with the next disjunctive in this level
			if (cur.noChoices()) {
				return false;
			}
			cur.decreCounter();
			cur.restore();
			cur.createBranch(ais);
			this.dc.modifyQueueContent(cur);
			// if(!this.dc.getIndividualsInQueue().contains(cur.getBranchInd())){
			this.dc.addToQueue(cur.getBranchInd(), InQueueOrder.INQUEUELAST);
			// }
		} else {
			// backtracking without exploring other branches
			return findBranchInStack(ind, ais);
		}
		return true;
	}

	private boolean findBranchInStack(Individual ind, Set<Integer> ais)
			throws BackjumpingNoDepSetException {
		// the current branch does not contribute to the clash,
		// backjumping without explore other branches
		// now backtrack to the last (most recent) branch
		Stack<Branching> allbrs = this.dc.getAllBranchesInPath();
		int ilen = allbrs.size();
		// find the most recent branching point
		Branching newcur = null;
		for (int i = ilen - 1; i >= 0; i--) {
			Branching br = allbrs.get(i);
			if (ais.contains(br.getOrder())) {
				newcur = br;
				break;
			}
		}
		if (newcur != null) {
			this.dc.setCurrentBranch(newcur);
			Branching last = allbrs.pop();
			while (!last.equals(newcur)) {
				// if(last.getBranchInd().getOrder()>=newcur.getBranchInd().getOrder()){
				//
				// allbrs.remove(last);
				// }
				last.restore();
				this.dc.modifyQueueContent(last);
				last = allbrs.pop();
			}
			return hasNextBranchingOd(ind, ais);
		} else
			throw new BackjumpingNoDepSetException("Unable to find a match!");
		// return false;
	}

	// private boolean backjumpToBranch(int upto, Set<Integer> ais){
	// Stack<Branching> allbrs = this.dc.getAllBranchesInPath();

	// Branching oldcur = this.dc.getCurrentBranching();
	// System.out.printf("Jumping from %d->%d\n", oldcur.getOrder(),
	// newcur.getOrder());
	// int length = allbrs.size();

	// newcur.restore();
	// boolean nomore = newcur.noChoices();
	// if(nomore){
	// return false;
	// }
	// restore all previous branches, starting from the most recent
	// pop up until the current branch is done
	// for(int i=0; i<(length-upto); i++){
	// allbrs.pop();
	// }

	// newcur.restore();
	// newcur.createBranch(ais);
	// if(!this.dc.getIndividualsInQueue().contains(newcur.getBranchInd())){
	// this.dc.addToQueue(newcur.getBranchInd(), InQueueOrder.INQUEUELAST);
	// }
	// return true;
	// }

}
